%
% Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
%
% SPDX-License-Identifier: BSD-2-Clause
%

@Article{dennis_vanhorn_66,
  author	= {Jack B. Dennis and Van Horn, Earl C.},
  title		= {Programming Semantics for Multiprogrammed Computations},
  journal	= cacm,
  year		= 1966,
  volume	= 9,
  pages		= {143--155},
  annote	= {The original capabilities paper.},
  heldby	= {gernot}
}

@InProceedings{boyton_09,
  author	= {Andrew Boyton},
  title		= {A Verified Shared Capability Model},
  booktitle	= ssv09,
  editor	= {Gerwin Klein and Ralf Huuck and Bastian Schlich},
  series	= entcs,
  volume	= {254},
  pages		= {25--44},
  publisher	= {Elsevier},
  year		= {2009},
  address	= {Aachen, Germany},
  month		= oct,
  format	= {pdf},
  keywords	= {nicta, l4verified, sel4},
  affiliation	= cseaffil # {\\}  # nictaaffil
}

@InProceedings{cock_08,
  author	= {David Cock},
  title		= {Bitfields and Tagged Unions in {C}: Verification through
		  Automatic Generation},
  booktitle	= verify08,
  year		= {2008},
  editor	= {Bernhard Beckert and Gerwin Klein},
  series	= {{CEUR} Workshop Proceedings},
  address	= {Sydney, Australia},
  volume	= 372,
  month		= aug,
  pages		= {44--55},
  keywords	= {nicta, l4verified},
  format	= {pdf}
}

@InProceedings{cock_ks_08,
  author	= {David Cock and Gerwin Klein and Thomas Sewell},
  title		= {Secure Microkernels, State Monads and Scalable
		  Refinement},
  editor	= {Otmane Ait Mohamed and C\'{e}sar Mu{\~{n}}oz and
		  Sofi\`{e}ne Tahar},
  series	= lncs,
  publisher	= {Springer},
  pages		= {167--182},
  volume	= {5170},
  booktitle	= tphols08,
  year		= {2008},
  address	= {Montreal, Canada},
  month		= aug,
  keywords	= {nicta, sel4, l4verified},
  format	= {pdf}
}

@InProceedings{derrin_ekcc_06,
  author	= {Philip Derrin and Kevin Elphinstone and Gerwin Klein and
		  David Cock and Manuel M. T. Chakravarty},
  title		= {Running the Manual: An Approach to High-Assurance
		  Microkernel Development},
  booktitle	= haskellws,
  year		= 2006,
  address	= {Portland, OR, USA},
  month		= sep,
  format	= {pdf},
  keywords	= {nicta, l4verified, sel4}
}

@TechReport{elkaduwe_ge_07,
  author	= {Dhammika Elkaduwe and Gerwin Klein and Kevin Elphinstone},
  title		= {Verified Protection Model of the {seL4} Microkernel},
  institution	= {NICTA},
  year		= 2007,
  month		= oct,
  note		= {Available from
		  \url{https://trustworthy.systems/publications/nicta_full_text/1474.pdf}}
		  ,
  format	= {pdf},
  number	= {NRL-1474},
  keywords	= {nicta, sel4, l4verified},
  heldby	= {dhammikae}
}

@InProceedings{elkaduwe_ge_08,
  author	= {Dhammika Elkaduwe and Gerwin Klein and Kevin Elphinstone},
  title		= {Verified Protection Model of the {seL4} Microkernel},
  booktitle	= vstte08,
  editor	= {Jim Woodcock and Natarajan Shankar},
  address	= {Toronto, Canada},
  publisher	= {Springer},
  year		= 2008,
  month		= oct,
  format	= {pdf},
  pages		= {99--114},
  series	= lncs,
  volume	= {5295},
  keywords	= {nicta, sel4, l4verified}
}

@InProceedings{elphinstone_kdrh_07,
  author	= {Kevin Elphinstone and Gerwin Klein and Philip Derrin and
		  Timothy Roscoe and Gernot Heiser},
  title		= {Towards a Practical, Verified Kernel},
  booktitle	= hotos07,
  year		= 2007,
  pages		= {117--122},
  address	= {San Diego, CA, USA},
  keywords	= {nicta, sel4, l4verified},
  month		= may,
  format	= {pdf}
}

@Article{heiser_ekkp_07,
  author	= {Gernot Heiser and Kevin Elphinstone and Ihor Kuz and
		  Gerwin Klein and Stefan M. Petters},
  title		= {Towards Trustworthy Computing Systems: Taking Microkernels
		  to the Next Level},
  journal	= osr,
  year		= 2007,
  month		= jul,
  volume	= {41},
  number	= {4},
  pages		= {3--11},
  format	= {pdf},
  keywords	= {nicta, okl, l4, sel4, l4verified, potoroo, camkes}
}

@Article{klein_09,
  oldlabel	= {Klein_08},
  author	= {Gerwin Klein},
  title		= {Operating System Verification --- An Overview},
  journal	= {S\={a}dhan\={a}},
  publisher	= {Springer},
  year		= 2009,
  keywords	= {nicta, l4verified},
  format	= {pdf},
  volume	= 34,
  number	= 1,
  month		= feb,
  pages		= {27--69},
  htmlnote	= {Invited paper. <a href="http://www.ias.ac.in/sadhana/"
		  class="no_highlight">Journal homepage.</a>}
}

@InProceedings{klein_de_09,
  author	= {Gerwin Klein and Philip Derrin and Kevin Elphinstone},
  title		= {Experience Report: {seL4} --- Formally Verifying a
		  High-Performance Microkernel},
  booktitle	= icfp09,
  year		= 2009,
  address	= {Edinburgh, UK},
  month		= aug,
  format	= {pdf},
  pages		= {91--96},
  keywords	= {nicta, sel4, l4verified},
  publisher	= {ACM}
}

@InProceedings{klein_ehacdeeknstw_09,
  author	= {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and
		  June Andronick and David Cock and Philip Derrin and
		  Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and
		  Michael Norrish and Thomas Sewell and Harvey Tuch and Simon
		  Winwood},
  title		= {{seL4}: Formal Verification of an {OS} Kernel},
  booktitle	= sosp09,
  publisher	= {ACM},
  year		= {2009},
  address	= {Big Sky, MT, USA},
  month		= oct,
  pages		= {207--220},
  format	= {pdf},
  keywords	= {best, nicta, okl, sel4, l4verified, l4vbest},
  htmlnote	= {<span class="important">Best Paper Award!</span>}
}

@Article{klein_ehacdeeknstw_10,
  author	= {Gerwin Klein and June Andronick and Kevin Elphinstone and
		  Gernot Heiser and David Cock and Philip Derrin and Dhammika
		  Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael
		  Norrish and Thomas Sewell and Harvey Tuch and Simon
		  Winwood},
  title		= {{seL4}: Formal Verification of an {OS} Kernel},
  journal	= cacm,
  publisher	= {ACM},
  year		= {2010},
  month		= jun,
  pages		= {107--115},
  volume	= 53,
  number	= 6,
  format	= {pdf},
  keywords	= {nicta, sel4, okl, l4verified, l4vbest}
}

@Article{tuch_09,
  author	= {Harvey Tuch},
  title		= {Formal verification of {C} systems code: Structured types,
		  separation logic and theorem proving},
  editor	= {Gerwin Klein and Ralf Huuck and Bastian Schlich},
  year		= 2009,
  keywords	= {nicta, l4verified},
  format	= {pdf},
  journal	= jar # {: Special Issue on Operating System Verification},
  volume	= {42},
  number	= {2--4},
  publisher	= {Springer},
  pages		= {125--187},
  affiliation	= cseaffil # {\\}  # nictaaffil # {\\}  # "now at VMWare",
  month		= apr
}

@InProceedings{tuch_08,
  author	= {Harvey Tuch},
  title		= {Structured Types and Separation Logic},
  booktitle	= ssv08,
  editor	= {Ralf Huuck and Gerwin Klein and Bastian Schlich},
  year		= {2008},
  address	= {Sydney, Australia},
  month		= feb,
  keywords	= {nicta, l4verified},
  format	= {pdf},
  series	= entcs,
  publisher	= {Elsevier},
  volume	= {217},
  pages		= {41--59},
  affiliation	= cseaffil # {\\}  # nictaaffil
}

@InProceedings{tuch_kh_05,
  author	= {Harvey Tuch and Gerwin Klein and Gernot Heiser},
  title		= {{OS} Verification --- Now!},
  booktitle	= hotos05,
  pages		= {7--12},
  year		= 2005,
  address	= {Santa Fe, NM, USA},
  format	= {pdf},
  keywords	= {nicta, L4, l4verified},
  month		= jun,
  organization	= usenix
}

@InProceedings{tuch_kn_07,
  author	= {Harvey Tuch and Gerwin Klein and Michael Norrish},
  title		= {Types, Bytes, and Separation Logic},
  booktitle	= popl07,
  year		= {2007},
  editor	= {Martin Hofmann and Matthias Felleisen},
  address	= {Nice, France},
  month		= jan,
  pages		= {97--108},
  keywords	= {best, nicta, l4verified, kmalloc, l4vbest},
  format	= {pdf},
  affiliation	= cseaffil # {\\}  # nictaaffil # {\\}  # nicta
		# {, Canberra, Australia}
}

@InProceedings{tuch_klein_05,
  author	= {Harvey Tuch and Gerwin Klein},
  title		= {A Unified Memory Model for Pointers},
  booktitle	= lpar05,
  pages		= {474--488},
  address	= {Montego Bay, Jamaica},
  format	= {pdf},
  keywords	= {nicta, L4, l4verified},
  month		= dec,
  year		= 2005
}

@PhDThesis{tuch:phd,
  author	= {Harvey Tuch},
  supervisor	= {gernot, kleing},
  title		= {Formal Memory Models for Verifying {C} Systems Code},
  school	= cse,
  year		= 2008,
  type		= {{PhD} Thesis},
  address	= unswadr,
  month		= aug,
  format	= {pdf},
  keywords	= {nicta, l4verified},
  affiliation	= cseaffil # {\\}  # nictaaffil
}

@InProceedings{winwood_ksacn_09,
  author	= {Simon Winwood and Gerwin Klein and Thomas Sewell and June
		  Andronick and David Cock and Michael Norrish},
  title		= {Mind the Gap: A Verification Framework for Low-Level {C}},
  booktitle	= tphols09,
  editor	= {Stefan Berghofer and Tobias Nipkow and Christian Urban and
		  Makarius Wenzel},
  year		= {2009},
  address	= {Munich, Germany},
  month		= aug,
  series	= lncs,
  volume	= {5674},
  publisher	= {Springer},
  keywords	= {nicta, l4verified},
  pages		= {500--515},
  format	= {pdf},
  affiliation	= cseaffil # {\\}  # nictaaffil
}

@Book{lncs2283,
  author	= {Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
  title		= "{Isabelle/HOL} --- A Proof Assistant for Higher-Order
		  Logic",
  publisher	= springer,
  series	= lncs,
  volume	= 2283,
  year		= 2002
}

@InProceedings{Matichuk_Murray_12,
  author =       {Daniel Matichuk and Toby Murray},
  title =        {Extensible Specifications for Automatic Re-Use of Specifications and Proofs},
  booktitle =    sefm12,
  series =       lncs,
  volume =       {7504},
  pages =        {333--341},
  year =         {2012},
  month =        oct,
  keywords =     {nicta, infoflow, ts},
  format =       {pdf}
}
